Nuprl Lemma : es-p-equiv_inversion 11,40
es, es':ES, P:(es:ESE). es  es' mod es,e.P(es,e)  es'  es mod es,e.P(es,e) 
latex

Definitionsx,y. t(x;y), x. t(x), P  Q, t  T, A c B, P  Q, P & Q, x(s1,s2), es  es' mod es,e.P(es;e), P  Q, , x:A. B(x), x(s), A  B
Lemmasevent system wf, es-p-equiv wf, es-same-val wf, subtype rel weakening, subtype rel transitivity, ext-eq inversion, es-causl wf, subtype rel set, es-E wf

origin